f:().
(n:. 0  f(n))
 (q:. (0 < q & (n:. m:. ((n < m) & q  f(m)))))
 (B:. n:. B  1  i < n. f(i)) 

latex

Definitions

i  j < k, {i..j}, (i = j), x f y, i <z j, Y, t.2, t.1, 0, +r, e, *, (op,id) lb  i < ub. E(i), r+gp,  lb  i < ub. E(i), <+*>, (r) i  k < j. E(k), a  j < b. E(j), P  Q, P  Q, {T}, SQType(T), True, T, A, A  B, A c B, ff, , tt, t  T, if b then t else f fi , x. t(x), , P & Q, x:A. B(x), x(s), P  Q, , x:A. B(x), P  Q, Dec(P), False, Unit, , S  T,

Lemmas

mon ident q, sum unroll lo q, sum unroll base q, ifthenelse wf, decidable int equal, int seg wf, qsum wf, true wf, squash wf, eq int wf, nat wf, false wf, qless wf, qle weakening eq qorder, int inc rationals, nat plus wf, qle wf, rationals wf, le wf, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, int-rational, assert of eq int, eqtt to assert, assert wf, iff transitivity, bool wf, q-not-limit-zero-diverges